/*
 * Atomic Predicates for Transformers
 * 
 * Copyright (c) 2015 UNIVERSITY OF TEXAS AUSTIN. All rights reserved. Developed
 * by: HONGKUN YANG and SIMON S. LAM http://www.cs.utexas.edu/users/lam/NRL/
 * 
 * Permission is hereby granted, free of charge, to any person obtaining a copy
 * of this software and associated documentation files (the "Software"), to deal
 * with the Software without restriction, including without limitation the
 * rights to use, copy, modify, merge, publish, distribute, sublicense, and/or
 * sell copies of the Software, and to permit persons to whom the Software is
 * furnished to do so, subject to the following conditions:
 * 
 * 1. Redistributions of source code must retain the above copyright notice,
 * this list of conditions and the following disclaimers.
 * 
 * 2. Redistributions in binary form must reproduce the above copyright notice,
 * this list of conditions and the following disclaimers in the documentation
 * and/or other materials provided with the distribution.
 * 
 * 3. Neither the name of the UNIVERSITY OF TEXAS AUSTIN nor the names of the
 * developers may be used to endorse or promote products derived from this
 * Software without specific prior written permission.
 * 
 * 4. Any report or paper describing results derived from using any part of this
 * Software must cite the following publication of the developers: Hongkun Yang
 * and Simon S. Lam, Scalable Verification of Networks With Packet Transformers
 * Using Atomic Predicates, IEEE/ACM Transactions on Networking, October 2017,
 * Volume 25, No. 5, pages 2900-2915 (first published as IEEE Early Access
 * Article, July 2017, Digital Object Identifier: 10.1109/TNET.2017.2720172).
 * 
 * 
 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
 * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
 * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
 * CONTRIBUTORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
 * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
 * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS WITH
 * THE SOFTWARE.
 */
package transformer;

import java.util.*;

import common.APComputer;
import common.BDDACLWrapper;
import common.Fields;
import common.FWDAPSet;
import jdd.bdd.BDD;

public class NATBox extends Box {

    class translation_entry{
        int field_bdd;
        int new_val_bdd;
        int old_pkt_bdd;

        translation_entry(int old_val, int field, int new_val)
        {
            old_pkt_bdd = old_val;
            field_bdd = field;
            new_val_bdd = new_val;
        }
    }

    ArrayList<translation_entry> nat_table_in;
    ArrayList<translation_entry> nat_table_out;

    // connects to the subnet
    static String port_in = "in";
    // connects to the internet
    static String port_out = "out";

    /**
     *  a predicate -> transformed predicate
     *  other predicate not shown in the HashMap are blocked
     */
    HashMap<Integer, Integer> translatedPredicates_in;
    HashMap<Integer, Integer> translatedPredicates_out;
    
    HashSet<Integer> computedPredicates_in;
    HashSet<Integer> computedPredicates_out;

    int[] beforeTranslation_in;
    FWDAPSet[] afterTranslation_in;
    HashMap<Integer, FWDAPSet> translatedPredicates_in_ap;

    int[] beforeTranslation_out;
    FWDAPSet[] afterTranslation_out;
    HashMap<Integer, FWDAPSet> translatedPredicates_out_ap;

    public void setaps(APComputer apc)
    {
        translatedPredicates_in_ap = new HashMap<Integer, FWDAPSet> ();
        setaps(apc, translatedPredicates_in, translatedPredicates_in_ap);

        beforeTranslation_in = new int[translatedPredicates_in_ap.size()];
        afterTranslation_in = new FWDAPSet[translatedPredicates_in_ap.size()];
        int ind = 0;
        for(int before: translatedPredicates_in_ap.keySet())
        {
            //System.out.println("in "+before);
            beforeTranslation_in[ind] = before;
            afterTranslation_in[ind] = translatedPredicates_in_ap.get(before);
            ind++;
        }

        translatedPredicates_out_ap = new HashMap<Integer, FWDAPSet> ();
        setaps(apc, translatedPredicates_out, translatedPredicates_out_ap);
        //System.out.println(translatedPredicates_out.size());

        beforeTranslation_out = new int[translatedPredicates_out_ap.size()];
        afterTranslation_out = new FWDAPSet[translatedPredicates_out_ap.size()];
        ind = 0;
        //System.out.println(translatedPredicates_out_ap.size());
        for(int before: translatedPredicates_out_ap.keySet())
        {
            //System.out.println("out "+before);
            beforeTranslation_out[ind] = before;
            afterTranslation_out[ind] = translatedPredicates_out_ap.get(before);
            ind++;
        }

    }

    private void setaps(APComputer apc, HashMap<Integer, Integer> predicate_table, HashMap<Integer, FWDAPSet> ap_table)
    {
        for(int beforetransform : predicate_table.keySet())
        {
            int after = predicate_table.get(beforetransform);
            HashSet<Integer> rawset = apc.getAPExpComputed(after);
            if(rawset == null)
            {
                System.err.println("bdd expression not found!");
                System.exit(1);
            }else
            {
                FWDAPSet aps = new FWDAPSet(rawset);
                ap_table.put(beforetransform, aps);
            }

        }
    }

    public void updateTranslatedPredicates(APComputer apc)
    {
        updateTranslatedPredicates(port_in, apc);
        updateTranslatedPredicates(port_out, apc);
    }

    private void updateTranslatedPredicates(String port, APComputer apc)
    {
        HashMap<Integer, Integer> translated = null;
        HashSet<Integer> computed = null;
        if(port.equals(port_in))
        {
            if(translatedPredicates_in == null)
            {
                translatedPredicates_in = new HashMap<Integer, Integer> ();
                computedPredicates_in = new HashSet<Integer> ();
            }
            translated = translatedPredicates_in;
            computed = computedPredicates_in;
        }else
        {
            if(translatedPredicates_out == null)
            {
                translatedPredicates_out = new HashMap<Integer, Integer> ();
                computedPredicates_out = new HashSet<Integer> ();
            }
            translated = translatedPredicates_out;
            computed = computedPredicates_out;
        }

        BDD bdd = baw.getBDD();
        for(int predicate : apc.getAllAP())
        {
            if(!computed.contains(predicate))
            {
                computed.add(predicate);
                
                HashMap<String, Integer> transforms = ForwardAction(port, predicate);
                int transformed = BDDACLWrapper.BDDFalse;
                for(int t : transforms.values())
                {
                    transformed = t;
                }
                    
                
                if(transformed != BDDACLWrapper.BDDFalse)
                {
                    if(transformed == predicate)
                    {
                        bdd.deref(transformed);
                    }else
                    {
                        //System.out.println(predicate+ " " + transformed);
                        translated.put(predicate, transformed);
                    }
                }
            }
            //System.out.println("------------");
        }
    }

    public void add_entry_in(int old_val, int field, int new_val)
    {
        translation_entry entry = new translation_entry(old_val, field, new_val);
        nat_table_in.add(entry);
    }

    public void add_entry_out(int old_val, int field, int new_val)
    {
        translation_entry entry = new translation_entry(old_val, field, new_val);
        nat_table_out.add(entry);
    }

    public NATBox(String name)
    {
        this.name = name;
        nat_table_in = new ArrayList<translation_entry> ();
        nat_table_out = new ArrayList<translation_entry> ();
    }

    public HashMap<String, FWDAPSet> ForwardAction(String port, FWDAPSet inpkts)
    {
        HashMap<String, FWDAPSet> fwded = new HashMap<String, FWDAPSet> ();

        if(port.equals(port_in))
        {
            //FWDAPSet outset = ForwardAction(inpkts, translatedPredicates_in_ap);
            FWDAPSet outset = ForwardAction(inpkts, beforeTranslation_in, afterTranslation_in);
            if(!outset.isempty())
            {
                fwded.put(port_out,  outset);
            }
        }else
        {
            //FWDAPSet outset = ForwardAction(inpkts, translatedPredicates_out_ap);
            FWDAPSet outset = ForwardAction(inpkts, beforeTranslation_out, afterTranslation_out);
            if(!outset.isempty())
            {
                fwded.put(port_in, outset);
            }
        }

        return fwded;
    }

    private FWDAPSet ForwardAction(FWDAPSet inpkts, HashMap<Integer, FWDAPSet> map_table)
    {
        FWDAPSet outset = new FWDAPSet(BDDACLWrapper.BDDFalse);

        for(int predicate : map_table.keySet())
        {
            if(inpkts.contains(predicate))
            {
                outset.union(map_table.get(predicate));
            }
        }

        return outset;
    }

    private FWDAPSet ForwardAction(FWDAPSet inpkts, int[] befores, FWDAPSet[] afters)
    {
        FWDAPSet outset = new FWDAPSet(BDDACLWrapper.BDDFalse);

        for(int i = 0; i < befores.length; i ++)
        {
            if(inpkts.contains(befores[i]))
            {
                outset.union(afters[i]);
            }
        }

        return outset;
    }

    public HashMap<String, Integer> ForwardAction(String port, int fwdp_raw)
    {
        HashMap<String, Integer> fwded = new HashMap<String, Integer> ();

        BDD theBDD = baw.getBDD();
        String outport = null;
        int res = BDDACLWrapper.BDDFalse;

        if(port.equals(port_in))
        {
            outport = port_out;
            for(translation_entry entry : nat_table_in)
            {
                int to_be_trans = theBDD.ref(theBDD.and(fwdp_raw, entry.old_pkt_bdd));
                int trans = baw.nat(to_be_trans, entry.field_bdd, entry.new_val_bdd);
                int tmp = theBDD.ref(theBDD.or(res, trans));

                theBDD.deref(to_be_trans);
                theBDD.deref(trans);
                theBDD.deref(res);

                res = tmp;
            }
        }

        if(port.equals(port_out))
        {
            outport = port_in;
            for(translation_entry entry : nat_table_out)
            {
                int to_be_trans = theBDD.ref(theBDD.and(fwdp_raw, entry.old_pkt_bdd));
                int trans = baw.nat(to_be_trans, entry.field_bdd, entry.new_val_bdd);
                int tmp = theBDD.ref(theBDD.or(res, trans));

                theBDD.deref(to_be_trans);
                theBDD.deref(trans);
                theBDD.deref(res);

                res = tmp;
            }

        }

        if(res != BDDACLWrapper.BDDFalse)
        {
            fwded.put(outport, res);
        }

        return fwded;
    }

    public static void main(String[] args)
    {
        // do some test
        BDDACLWrapper baw = new BDDACLWrapper();
        NATBox box = new NATBox("test");
        NATBox.baw = baw;

        int new_addr = baw.encodeDstIPPrefix(127, 32);
        int old_pkt = baw.encodeDstIPPrefix(255, 32);
        box.add_entry_in(old_pkt, baw.get_field_bdd(Fields.dst_ip), new_addr);
        box.add_entry_out(old_pkt, baw.get_field_bdd(Fields.dst_ip), new_addr);

        System.out.println("new packet:" + new_addr);
        System.out.println(box.ForwardAction(NATBox.port_out, old_pkt).get(NATBox.port_in));

    }

}
